Here we prove that given an \evols{3} process $P$ 
its associated Petri net representation \pnr{P}{\emptyset}
faithfully preserves its behavior.
We need some auxiliary propositions and definitions.
The following proposition states how to build a Petri net for the parallel composition of two processes starting from the Petri nets of the two processes. 

\begin{proposition}\label{p:pn-pc}
Let  $P_1$ and $P_2$ 
be
two  \evols{3} processes with 
associated Petri nets $\pnr{P_1}{\emptyset}$ and $\pnr{P_2}{\emptyset}$, as in Definition \ref{d:pn}.
Then, the Petri net \pnr{P_{1} \parallel P_{2}}{\emptyset} is defined as:
$$\pnr{P_{1} \parallel P_{2}}{\emptyset} = (\places{P_{1} \parallel P_{2}}, \transit{P_{1} \parallel P_{2}}, \initMark{P_{1} \parallel P_{2}})$$
where 
\begin{align*}
\places{P_{1} \parallel P_{2},\emptyset}&=\places{P_1, \emptyset} \cup \places{P_2, \emptyset},\\
\transit{P_{1} \parallel P_{2},\emptyset}& =  \transit{P_1, \emptyset} \cup \transit{P_2, \emptyset} \cup T,\\
\initMark{P_{1} \parallel P_{2}}&=\initMark{P_1} \uplus \initMark{P_2}
\end{align*}
with $T$ representing the set of instances of transition schemata in Table \ref{tab:pn} 
that become possible 
due to the interplay of places in $\places{P_1, \emptyset}$ and in $\places{P_2, \emptyset}$. % parallel composition as defined in Definition \ref{d:pn}. 
%\todo{Maybe a more formal description?}
\end{proposition}

\begin{proof}
Immediate from the definitions.
\end{proof}

Similarly, the next proposition shows how to obtain the Petri net associated to $\component{a}{P}$ starting from the one of $P$.

\begin{proposition}\label{p:pn-ap}
Let  $P$ 
be
an \evols{3} process with 
associated Petri net $\pnr{P}{\emptyset}$ as in Definition \ref{d:pn}.
Then, the Petri net \pnr{\component{a}{P}}{\emptyset}
is defined as:
$$ \pnr{\component{a}{P}}{\emptyset} = (\places{\component{a}{P}}, \transit{\component{a}{P}}, \initMark{\component{a}{P}})$$
where:
\begin{itemize}
\item $\places{\component{a}{P},\emptyset}=\{ \coppia{Q}{a\sigma} \mid  \coppia{Q}{\sigma} \in \places{P, \emptyset}\} \cup 
\{a \sigma \mid \sigma \in  \places{P, \emptyset} \}$ $\cup
\{ a \}$.
\item $\transit{\component{a}{P}}$ is obtained from $\transit{P,\emptyset}$ by replacing places in $\places{P, \emptyset}$ with places in $\places{\component{a}{P},\emptyset}$, as defined above.
\item $\initMark{\component{a}{P}}$ is obtained from $\initMark{P}$ by 
(i) replacing places in $\places{P, \emptyset}$ with places in $\places{\component{a}{P},\emptyset}$, as defined above, 
and (ii)  adding a token in  the place for the adaptable process $a$.
\end{itemize}
\end{proposition}
\begin{proof}
Immediate from the definitions.
\end{proof}






\begin{lemma}\label{l:auxpn}
 Let $P$ and $(\places{P,\emptyset}, \transit{P,\emptyset}, \initMark{P})$
 be an \evols{3} process and its associated Petri net,  as in Definition \ref{d:pn}.
 Then we have:
\begin{enumerate}
\item If $P \pired P'$ then $\decc{\varepsilon}{P} \uplus \{go\} \rightarrow  \decc{\varepsilon}{P'} \uplus \{go\}$.

\item If $\decc{\varepsilon}{P} \uplus \{go\} \rightarrow  m\uplus \{go\}$ then, for some $P'$, 
%implies that there exists $P'$  such that  
$P \pired P' \text{ and } \decc{\varepsilon}{P'}=m$
\end{enumerate}

\end{lemma}
\begin{proof}
The proof of  (1) proceeds by induction on the derivation tree of $P \pired P'$, with a case analysis on the last applied rule. 
There are seven cases to check. 
%We detail only the ones in which the reduction can be inferred with rules $\rulename{Act1}$, $\rulename{Loc}$, $\rulename{Tau1}$ and $\rulename{Tau3}$. The others are symmetric, and can be treated analogously.

\begin{description}
 \item [Case \rulename{Act1}:] Then we have $P = P_1 \parallel P_2$ and:
$$  
\inferrule{P_1 \arro{~~} P_1'}{P_1 \parallel P_2 \arro{\ } P'_1 \parallel P_2}			
$$
By inductive hypothesis,  we have $\decc{\varepsilon}{P_1} \uplus \{go\} \rightarrow  \decc{\varepsilon}{P_1'} \uplus \{go\}.$
By Proposition \ref{p:pn-pc},
$\transit{P_{1},\emptyset} \subseteq \transit{P_{1} \parallel P_{2},\emptyset}$.
Since by Definition \ref{d:pn} $\decc{\varepsilon}{P_1 \parallel P_2}  =  \decc{\varepsilon}{P_1} \uplus \decc{\varepsilon}{P_2}$,
 % and following from  Proposition \ref{p:pn-pc} 
then we can conclude that $\decc{\varepsilon}{P} \uplus \{go\} \rightarrow \decc{\varepsilon}{P'} \uplus \{go\} $ with $\decc{\varepsilon}{P'}=\decc{\varepsilon}{P_1'} \uplus \decc{\varepsilon}{P_2}$.
This concludes the proof for this case.
%\todo{The reasoning is not very clear...}

 \item [Case \rulename{Act2}:] Analogous to the case for \rulename{Act1} and omitted. 

 \item [Case \rulename{Loc}:] Then we have $P=\component{a}{P_1}$ and
$$  
\inferrule{P_1 \arro{~~} P_1'}{\component{a}{P_1} \arro{~~}  \component{a}{P_1'}}
$$
By inductive hypothesis, we have  $\decc{\varepsilon}{P_1} \uplus \{go\} \rightarrow  \decc{\varepsilon}{P_1'} \uplus \{go\}$.
Proposition \ref{p:pn-ap} states that 
%Remark \ref{remark:petri} 
$\transit{P,\emptyset}$ is obtained by extending the addresses of places
in $\transit{P_{1},\emptyset}$ with name $a$.
Since by Definition \ref{d:pn} $\decc{\varepsilon}{\component{a}{P_1}}  =  \decc{a}{P_1} \uplus \{a\}$ %and following from the Proposition \ref{p:pn-ap} 
then we can conclude that $\decc{\varepsilon}{P} \uplus \{go\} \rightarrow \decc{\varepsilon}{P'} \uplus \{go\} $ with $\decc{\varepsilon}{P'}=\decc{a}{P_1'} \uplus \{a\}$. This concludes the proof for this case.
%\todo{This needs to be more precise (and less verbose)}

\item [Cases \rulename{Tau1}-\rulename{Tau2}:]
Then $P \equiv  \fillcont{C_1}{A}\parallel \fillcont{C_2}{B}$, where $C_{1}, C_{2}$ are monadic contexts as in Definition \ref{d:mc}.
Moreover, 
$A$ is either 
$!b.Q$ or 
$\sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=b$, for some $l\in I$, and 
$B$ is either 
$!\outC{b}.R$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{b}$, for some $l\in I$.

We consider only the case in which $A = \sum_{i \in I} \pi_i.Q_i$ and $B = !\outC{b}.R$;  the other cases are similar. 
Let us denote with $\sigma$ and $\theta$ 
the address (with respect to the hole) induced by adaptable processes in $C_{1}$ and $C_{2}$, respectively.
That is, the address of $A$ in $C_{1}$ is $\sigma$ and the address of $B$ in $C_{2}$ is $\theta$.
%Suppose that $A$ is located inside a certain number of adaptable processes in context $C_1$ that generates the address $\sigma$. Similarly, suppose that $B$ is located at address $\theta$ in context $C_2$. 
Then, by construction of the Petri net, there is a token in the places $\coppia{\sum_{i \in I} \pi_i.Q_i}{\sigma}$ and $\coppia{!\outC{b}.R}{\theta}$.
Therefore,  transition 
$$\{go, \coppia{\sum_{i \in I} \pi_i.Q_i}{\sigma},
        \coppia{!\outC{b}.R}{\theta}\}
         \derriv
\{go, \coppia{!\outC{b}.R}{\theta}\} \uplus
\decc{\theta}{R} \uplus \decc{\sigma}{Q_{l}}
$$
(denoted (4) in Table~\ref{tab:pn}) can fire.
By definition of $\mathsf{dec}$ (cf. Definition \ref{d:pn})
it is easy to see that this corresponds to $\decc{\varepsilon}{P'} \uplus \{go\}$. This concludes the proof for this case.
 
\item [Cases \rulename{Tau3}-\rulename{Tau4}:]
Then $P \equiv \fillcont{C_1}{A} \parallel \fillcont{C_2}{B}$ where:
\begin{itemize}
\item $C_{1},C_{2}$ are monadic contexts, as in Definition \ref{d:mc}; 
\item $A = \component{b}{P_1}$, for some $P_{1}$;  
\item $B  =  \sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{b}{\component{b}{U} \parallel P_2}$ for $l\in I$, or $ B = !\update{b}{\component{b}{U} \parallel P_2}.R$, for some $P_{2}, R$.
\end{itemize}


%Thus, there are two sub-cases; 
We consider the case in which $B = !\update{b}{\component{b}{U} \parallel P_2}.R$; the other case is similar. 
Let us denote with $\sigma$ and $\theta$ 
the address (with respect to the hole) induced by adaptable processes in $C_{1}$ and $C_{2}$, respectively.
That is, the address of $A$ in $C_{1}$ is $\sigma$ and the address of $B$ in $C_{2}$ is $\theta$.
Then, by construction of the Petri net, 
we have a token in the places $\{\sigma b\}$ and $\coppia{!\update{b}{\component{b}{U} \parallel P_2}.R}{\theta}$. 
At this point, we should distinguish two cases, depending on whether $\sigma b$ is contained in $\theta$ or not.
Suppose $\sigma b$ is not contained in $\theta$. That is, there is no process with the nesting structure of $C_{1}$ inside $C_{2}$.
Then   transition 
$$
\begin{array}{ll}
\{go, \sigma b, \coppia{!\update{b}{\component{b}{U} \parallel P_2}.R}{\theta} \}
 \derriv&
 \{go, \coppia{!\update{b}{\component{b}{U} \parallel P_2}.R}{\theta} ,\sigma b\} \uplus \\
 &\decc{\theta}{R} \uplus 
 \decc{\sigma }{P_2} 
 \uplus \decc{\sigma b}{U} 
 \end{array}
              $$
(denoted (8) in Table~\ref{tab:pn}) can fire.
It easy to see that this corresponds to $\decc{\varepsilon}{P'} \uplus \{go\}$ and we are done.

Similarly,  if $\sigma b$ is contained in $\theta$ then it means that there exists a process with the same structure of $C_1$ inside $C_2$.
Therefore, the place $\sigma b$ is duplicated and a token is present in both places. Then transition 
$$
\begin{array}{ll}
\{go, \sigma b, \sigma b, \coppia{!\update{b}{\component{b}{U} \parallel P_2}.R}{\theta}, \}
 \derriv \!\!\!&
 \{go, \sigma b, \sigma b,  \coppia{!\update{b}{\component{b}{U} \parallel P_2}.R}{\theta} \} \uplus \\
 &\decc{\theta}{R} \uplus 
 \decc{\sigma }{P_2} 
 \uplus \decc{\sigma b}{U} 
  \end{array}
              $$
(denoted (9) in Table~\ref{tab:pn}) can fire.
It easy to see that this corresponds to $\decc{\varepsilon}{P'} \uplus \{go\}$ and this concludes the proof.
\end{description}

We now move on the proof of (2), which proceeds by a case analysis on the transition fired by the Petri net. 
The transition schemata in 
Table~\ref{tab:pn}
can be divided into two groups: (1) transitions mimicking a synchronization (i.e., an interaction between  
an input and an output prefix)
and (2) transitions mimicking an update action
(i.e., an interaction between  
an update prefix and an adaptable process). We consider these two groups separately:

\begin{enumerate}
 
 \item  This group comprises transition schemata (3)--(5) in Table~\ref{tab:pn}.
 For simplicity we concentrate only on transitions of kind (3), as the others are similar.
If a transition of this kind can fire, then we have tokens in  $$\{go, \sum_{i \in I} \coppia{\pi_i.A_i}{\alpha},\sum_{j \in J} \coppia{\rho_j.B_j}{\beta}\}$$
which, by construction of the Petri net, 
implies that 
$$P \equiv \fillcont{D}{\sum_{i \in I}\pi_i.A_i,  \sum_{j \in J}\rho_j.B_j}$$
where $D$ is a biadic context, as in Definition \ref{d:mc}.
After the fire of the transition, tokens move to 
$\{go\}\uplus \decc{\alpha}{A_{l}} \uplus \decc{\beta}{B_{m}}$; by construction, 
this  corresponds to a process $P' \equiv \fillcont{D}{A_l, A_m}$, and we are done.

 \item  This group comprises transition schemata (6)--(9) in Table~\ref{tab:pn}.
For simplicity, we concentrate only on transitions of kind (6), as the others are similar.  
If a transition of this kind can fire, then we have tokens in   $$\{go, \coppia{\sum_{i \in I} \pi_i.A_i}{\alpha},\beta a\}$$ 
which, by construction of the Petri net, implies 
$$P\equiv \fillcont{D}{\sum_{i \in I}\pi_i.A_i, \component{a}{Q} }$$ where $D$ is a biadic context, as in Definition \ref{d:mc}.
After the fire of the transition the tokens move to $\{go\} \uplus \decc{\alpha}{A_{l}} \uplus \decc{\beta}{A}  \uplus \decc{\beta a}{U} \uplus \{\beta a\}$;
by construction, this corresponds to a process $P' \equiv \fillcont{D}{A_l, \component{a}{\fillcon{U}{Q}} \parallel A} $, and we are done.
\end{enumerate}
\end{proof}

We can now restate Lemma \ref{l:pn}, as in page \pageref{l:pn}:
\begin{lemma}[\ref{l:pn}]
 Let $P$ and $(\places{P,\emptyset}, \transit{P,\emptyset}, \initMark{P})$
 be an \evols{3} process and its associated Petri net,  as in Definition \ref{d:pn}.
 Then we have:
$$P \pired P' \textrm{ iff } \decc{\varepsilon}{P} \uplus \{go\} \rightarrow  \decc{\varepsilon}{P'} \uplus \{go\}.$$
\end{lemma}
\begin{proof}
Immediate from Lemma \ref{l:auxpn}.
\end{proof}
